\begin{tabbing}
should{-}forward(${\it es}$; ${\it In}$; ${\it isupdate}$; $f$; $a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\uparrow$($a$ $\in_{b}$ ${\it In}$)) \& ($\uparrow$(${\it isupdate}$(${\it In}$($a$)))))\+
\\[0ex]$\vee$ (($\neg$($\uparrow$($a$ $\in_{b}$ ${\it In}$))) \& ($\neg$(es{-}loc(${\it es}$; ($f$($a$))) = es{-}loc(${\it es}$; $a$) $\in$ Id)))
\-
\end{tabbing}